M:MsgA. Trans(M)  k:KndM.da(k)M.stateM.state 

latex

Definitions	t  T, Valtype(da;k), State(ds), IdDeq, Id, x:A. B(x), Type, Void, f(x)?z, Top, x:AB(x), Knd, <a,b>, 2of(t), KindDeq, product-deq(A;B;a;b), x:AB(x), x.A(x), x. t(x), 1of(t), P  Q, f(x), f(a), b, A, b, , s = t, Prop, a:A fp B(a), x  dom(f), P & Q, P  Q, Unit, left+right, M.ef(k,x,s,v)?w, Trans(M), M.state, M.da(a), MsgA
Lemmas	msga wf, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf, fpf-ap wf, ma-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, pi2 wf, product-deq wf, Knd wf, Kind-deq wf, fpf-cap-void-subtype, Id wf, id-deq wf